<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
	<head>
		<title>Type Check Propositions</title>
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
		<meta name="viewport" content="width=device-width initial-scale=1">
		<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
		<meta http-equiv="Content-Language" content="en-gb">

<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script>
MathJax = {
	tex: {
		inlineMath: '$', '$'], ['\\(', '\\)'
	},
	svg: {
		fontCache: 'global'
	}
};
</script>
<script type="text/javascript" id="MathJax-script" async
	src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>

<script>
function togglePopup(material_id) {
  var popup = document.getElementById(material_id);
  popup.classList.toggle("show");
}
</script>

<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
		
	</head>
	<body class="commentary-font">
		<nav role="navigation">
		<h1><a href="../index.html"><img src="../docs-assets/Inform.png" height=72> </a></h1>
<ul><li><a href="../index.html">home</a></li>
</ul><h2>Compiler</h2><ul>
<li><a href="../structure.html">structure</a></li>
<li><a href="../inbuildn.html">inbuild</a></li>
<li><a href="../inform7n.html">inform7</a></li>
<li><a href="../intern.html">inter</a></li>
<li><a href="../services.html">services</a></li>
<li><a href="../secrets.html">secrets</a></li>
</ul><h2>Other Tools</h2><ul>
<li><a href="../inblorbn.html">inblorb</a></li>
<li><a href="../inform6.html">inform6</a></li>
<li><a href="../inpolicyn.html">inpolicy</a></li>
</ul><h2>Resources</h2><ul>
<li><a href="../extensions.html">extensions</a></li>
<li><a href="../kits.html">kits</a></li>
</ul><h2>Repository</h2><ul>
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=0> github</a></li>
</ul><h2>Related Projects</h2><ul>
<li><a href="https://github.com/ganelson/inweb"><img src="../docs-assets/github.png" height=0> inweb</a></li>
<li><a href="https://github.com/ganelson/intest"><img src="../docs-assets/github.png" height=0> intest</a></li>
</ul>
		</nav>
		<main role="main">
		<!-- Weave of 'Type Check Propositions' generated by inweb -->
<div class="breadcrumbs">
    <ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#4">Chapter 4: Propositions</a></li><li><b>Type Check Propositions</b></li></ul></div>
<p class="purpose">Predicate calculus is a largely symbolic exercise, and its rules of working tend to assume that all predicates are meaningful for all terms: this means, for instance, that "if blue is 14" is likely to make a well-formed sentence in predicate calculus. In this section we reject such propositions on the grounds that they violate type-checking requirements on relations -- in this example, the equality relation.</p>

<ul class="toc"><li><a href="4-tcp.html#SP2">&#167;2. Problem reporting kit</a></li><li><a href="4-tcp.html#SP4">&#167;4. Type-checking whole propositions</a></li><li><a href="4-tcp.html#SP4_1">&#167;4.1. Finding kinds for variables</a></li><li><a href="4-tcp.html#SP5">&#167;5. The kind of a term</a></li><li><a href="4-tcp.html#SP8">&#167;8. Type-checking predicates</a></li><li><a href="4-tcp.html#SP10">&#167;10. Two problem messages needed more than once</a></li></ul><hr class="tocbar">

<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. </b>We can unambiguously find the kind of value of any constant \(C\), so if a
proposition's terms are all constant then type-checking is easy. ${\it is}(4, <span class="extract"><span class="extract-syntax">score</span></span>)$
good, ${\it is}(4, <span class="extract"><span class="extract-syntax">"fish"</span></span>)$ bad. The subtlety comes in interpreting
\({\it is}(4, x)\), where \(x\) is a variable. Our calculus allows variables to
range over many domains &mdash; numbers, texts, scenes, objects, and so on.
</p>

<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. Problem reporting kit.</b>The caller to <span class="extract"><span class="extract-syntax">TypecheckPropositions::type_check</span></span> has to fill this form out first. Paperwork,
what can you do, eh?
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">DECLINE_TO_MATCH</span><span class="plain-syntax"> </span><span class="constant-syntax">1000</span><span class="plain-syntax"> </span><span class="comment-syntax"> not one of the three legal </span><span class="extract"><span class="extract-syntax">*_MATCH</span></span><span class="comment-syntax"> values</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">NEVER_MATCH_SAYING_WHY_NOT</span><span class="plain-syntax"> </span><span class="constant-syntax">1001</span><span class="plain-syntax"> </span><span class="comment-syntax"> not one of the three legal </span><span class="extract"><span class="extract-syntax">*_MATCH</span></span><span class="comment-syntax"> values</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">typedef</span><span class="plain-syntax"> </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">issue_error</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">struct</span><span class="plain-syntax"> </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">ew_text</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">intention</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">log_to_I6_text</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">flag_problem</span><span class="plain-syntax">;</span>
<span class="plain-syntax">} </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax">;</span>

<span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::tc_no_problem_reporting</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::tc_no_problem_reporting</span></span>:<br/><a href="4-tcp.html#SP3">&#167;3</a><br/>Sentence Conversions - <a href="5-sc.html#SP10_1_1">&#167;10.1.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">void</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">issue_error</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">ew_text</span><span class="plain-syntax"> = </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">intention</span><span class="plain-syntax"> = </span><span class="string-syntax">"be silent checking"</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">flag_problem</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::tc_problem_reporting</span><span class="plain-syntax">(</span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax">, </span><span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">intent</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP2" class="function-link"><span class="function-syntax">TypecheckPropositions::tc_no_problem_reporting</span></a><span class="plain-syntax">();</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">issue_error</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">ew_text</span><span class="plain-syntax"> = </span><span class="identifier-syntax">W</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">intention</span><span class="plain-syntax"> = </span><span class="identifier-syntax">intent</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<ul class="endnotetexts"><li>The structure tc_problem_kit is private to this section.</li></ul>
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. </b>A version used only for the internal testing mode, when we print the outcome
into the debugging log, but diverted to an I6 string in the compiled code.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::tc_problem_logging</span><span class="plain-syntax">(</span><span class="reserved-syntax">void</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP2" class="function-link"><span class="function-syntax">TypecheckPropositions::tc_no_problem_reporting</span></a><span class="plain-syntax">();</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">intention</span><span class="plain-syntax"> = </span><span class="string-syntax">"be internal testing"</span><span class="plain-syntax">; </span><span class="identifier-syntax">tck</span><span class="plain-syntax">.</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. Type-checking whole propositions.</b>This section provides a single routine to the rest of Inform: <span class="extract"><span class="extract-syntax">TypecheckPropositions::type_check</span></span>.
We determine the kinds for all variables, then work through the proposition,
ensuring that every predicate-like atom has terms which match at least one
possible reading of the meaning of the atom.
</p>

<p class="commentary">As usual in Inform, type-checking is not a passive process. If it can make
sense of the proposition by changing it, it will do so.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::type_check</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::type_check</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP10_1_1">&#167;10.1.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> </span><span class="identifier-syntax">tck_s</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax"> </span><span class="identifier-syntax">vta</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax"> = &amp;</span><span class="identifier-syntax">tck_s</span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"Type-checking proposition: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-bas.html#SP2" class="function-link"><span class="function-syntax">Binding::is_well_formed</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"type-checking malformed proposition"</span><span class="plain-syntax">);</span>

<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_1" class="named-paragraph-link"><span class="named-paragraph">First make sure any constants in the proposition have themselves been typechecked</span><span class="named-paragraph-number">4.1</span></a></span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_2" class="named-paragraph-link"><span class="named-paragraph">Look at KIND atoms to see what kinds of value are asserted for the variables</span><span class="named-paragraph-number">4.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_3" class="named-paragraph-link"><span class="named-paragraph">Look at KIND atoms to reject unarticled shockers</span><span class="named-paragraph-number">4.3</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_4" class="named-paragraph-link"><span class="named-paragraph">Assume any still-unfathomable variables represent objects</span><span class="named-paragraph-number">4.4</span></a></span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;pl-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) </span><a href="4-tcp.html#SP5" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]), &amp;</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">flag_problem</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">))</span>
<span class="plain-syntax">            </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_6" class="named-paragraph-link"><span class="named-paragraph">A binary predicate is required to apply to terms of the right kinds</span><span class="named-paragraph-number">4.6</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">))</span>
<span class="plain-syntax">            </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_5" class="named-paragraph-link"><span class="named-paragraph">A unary predicate is required to have an interpretation matching the kind of its term</span><span class="named-paragraph-number">4.5</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">) </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_7" class="named-paragraph-link"><span class="named-paragraph">Show the variable assignment in the debugging log</span><span class="named-paragraph-number">4.7</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP4_1" class="paragraph-anchor"></a><b>&#167;4.1. Finding kinds for variables.</b>Every specification compiled by Inform has to pass through type-checking.
That includes the ones which occur as constants inside propositions, and this is
where.
</p>

<p class="commentary">The presence of an <span class="extract"><span class="extract-syntax">UNKNOWN_NT</span></span> constant indicates something which failed to be
recognised by the S-parser. That shouldn't happen, but we allow for it so that
we can recover from an already reported problem.
</p>

<p class="commentary">Perhaps surprisingly, we don't reject generic constants: this is so that
sentences like
</p>

<blockquote>
    <p>A thing usually weighs 10kg.</p>
</blockquote>

<p class="commentary">...can work &mdash; here the generic constant for "thing" is treated as a noun,
since it can be the subject of inferences all by itself. So it can legitimately
be a term in a proposition.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">First make sure any constants in the proposition have themselves been typechecked</span><span class="named-paragraph-number">4.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;pl-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::constant_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]));</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">spec</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (!(</span><span class="identifier-syntax">Node::is</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">UNKNOWN_NT</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">issue_error</span><span class="plain-syntax">) </span><span class="identifier-syntax">rv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Dash::check_value</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Dash::check_value_silently</span><span class="plain-syntax">(</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">                #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">                #</span><span class="identifier-syntax">ifndef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">rv</span><span class="plain-syntax"> = </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">rv</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_1_1" class="named-paragraph-link"><span class="named-paragraph">Recover from problem in S-parser by not issuing problem</span><span class="named-paragraph-number">4.1.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_2" class="paragraph-anchor"></a><b>&#167;4.2. </b>If the proposition contains contradictory <span class="extract"><span class="extract-syntax">KIND</span></span> atoms, it automatically fails
type-checking, even if there is no implication that both apply at once. This
throws out, for instance:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="constant-syntax">1</span><span class="plain-syntax">. </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">scene</span><span class="plain-syntax"> </span><span class="identifier-syntax">which</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">not</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> </span><span class="identifier-syntax">number</span>
<span class="plain-syntax">    [ </span><span class="identifier-syntax">scene</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) &amp; </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">[ </span><span class="identifier-syntax">number</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">] ]</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">Failed:</span><span class="plain-syntax"> </span><span class="identifier-syntax">proposition</span><span class="plain-syntax"> </span><span class="identifier-syntax">would</span><span class="plain-syntax"> </span><span class="identifier-syntax">not</span><span class="plain-syntax"> </span><span class="identifier-syntax">type</span><span class="plain-syntax">-</span><span class="identifier-syntax">check</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">x</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">both</span><span class="plain-syntax"> </span><span class="identifier-syntax">scene</span><span class="plain-syntax"> </span><span class="identifier-syntax">and</span><span class="plain-syntax"> </span><span class="identifier-syntax">number</span>
</pre>
<p class="commentary">It could be argued that all scenes ought to pass this proposition, but we will
treat it as a piece of nonsense, like "if Wednesday is not custard".
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Look at KIND atoms to see what kinds of value are asserted for the variables</span><span class="named-paragraph-number">4.2</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_kind</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::is_object</span><span class="plain-syntax">(</span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">)) </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">old_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">];</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">old_kind</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::compatible</span><span class="plain-syntax">(</span><span class="identifier-syntax">old_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                            </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"%c is both %u and %u\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">], </span><span class="identifier-syntax">old_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                        </span><a href="4-tcp.html#SP10" class="function-link"><span class="function-syntax">TypecheckPropositions::issue_kind_typecheck_error</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">old_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                    }</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::Behaviour::definite</span><span class="plain-syntax">(</span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">old_kind</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">v</span><span class="plain-syntax">] = </span><span class="identifier-syntax">new_kind</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_3" class="paragraph-anchor"></a><b>&#167;4.3. </b>The following is arguably a problem which should have been thrown earlier,
but it's a very subtle one, and we want to use it only when everything else
(more or less) has worked.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Look at KIND atoms to reject unarticled shockers</span><span class="named-paragraph-number">4.3</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP5" class="function-link"><span class="function-syntax">KindPredicates::is_unarticled_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Rejecting as unarticled\n"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">issue_error</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">BareKindVariable_CALCERROR</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_4" class="paragraph-anchor"></a><b>&#167;4.4. </b>It's possible for a proposition to specify nothing about the kind of a
variable (usually a free one). If so, it's assumed to be an object. For
instance, if we define
</p>

<blockquote>
    <p>Definition: a container is empty if the number of things in it is 0.</p>
</blockquote>

<p class="commentary">then we find that, say:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="constant-syntax">1</span><span class="plain-syntax">. </span><span class="identifier-syntax">empty</span><span class="plain-syntax"> </span><span class="identifier-syntax">which</span><span class="plain-syntax"> </span><span class="identifier-syntax">is</span><span class="plain-syntax"> </span><span class="identifier-syntax">empty</span>
<span class="plain-syntax">    [ </span><span class="character-syntax">'empty'</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) &amp; </span><span class="character-syntax">'empty'</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) ]</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">x</span><span class="plain-syntax"> (</span><span class="identifier-syntax">free</span><span class="plain-syntax">) - </span><span class="identifier-syntax">object</span><span class="plain-syntax">.</span>
</pre>
<p class="commentary">though in fact it would also have been viable for \(x\) to be a rulebook, a list,
or various other kinds of value.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Assume any still-unfathomable variables represent objects</span><span class="named-paragraph-number">4.4</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_1_1" class="paragraph-anchor"></a><b>&#167;4.1.1. </b>The following is really rather paranoid; it ought to be certain that a
problem message has already been issued, but just in case not...
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Recover from problem in S-parser by not issuing problem</span><span class="named-paragraph-number">4.1.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">problem_count</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Atom $o contains failed constant\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">issue_error</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">ConstantFailed_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4_1">&#167;4.1</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_5" class="paragraph-anchor"></a><b>&#167;4.5. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">A unary predicate is required to have an interpretation matching the kind of its term</span><span class="named-paragraph-number">4.5</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-upf.html#SP3" class="function-link"><span class="function-syntax">UnaryPredicateFamilies::typecheck</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"UP $o cannot be applied\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_6" class="paragraph-anchor"></a><b>&#167;4.6. </b>The BP case is interesting because it forgives a failure in one case: of
\({\it is}(t, C)\), where \(C\) is a constant representing a value of an enumerated
kind. Sentence conversion is actually quite good at distinguishing these cases
and can see the difference between "the bus is red" and "the fashionable hue
is red", but it is defeated by cases where adjectives representing values are
used about other values &mdash; "the Communist Rally is red", where "Communist
Rally" is a scene rather than an object, for instance. We first try requiring
<span class="extract"><span class="extract-syntax">Rally</span></span> to be a colour: when that fails, we see if the atom ${\it red}(<span class="extract"><span class="extract-syntax">Rally</span></span>)$
would work instead. If it would, we make the change within the proposition.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">A binary predicate is required to apply to terms of the right kinds</span><span class="named-paragraph-number">4.6</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="3-bp.html#SP16" class="function-link"><span class="function-syntax">BinaryPredicates::is_the_wrong_way_round</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">)) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"BP wrong way round"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-tcp.html#SP9" class="function-link"><span class="function-syntax">TypecheckPropositions::type_check_binary_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">R_equality</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">alt</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP10" class="function-link"><span class="function-syntax">Terms::noun_to_adj_conversion</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1]);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">alt</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> </span><span class="identifier-syntax">test_unary</span><span class="plain-syntax"> = *</span><span class="identifier-syntax">pl</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">test_unary</span><span class="plain-syntax">.</span><span class="element-syntax">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">test_unary</span><span class="plain-syntax">.</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">alt</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-tcp.html#SP8" class="function-link"><span class="function-syntax">TypecheckPropositions::type_check_unary_predicate</span></a><span class="plain-syntax">(&amp;</span><span class="identifier-syntax">test_unary</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_6_1" class="named-paragraph-link"><span class="named-paragraph">The BP fails type-checking</span><span class="named-paragraph-number">4.6.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> = </span><span class="constant-syntax">1</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax"> = </span><span class="identifier-syntax">STORE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">alt</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_6_1" class="named-paragraph-link"><span class="named-paragraph">The BP fails type-checking</span><span class="named-paragraph-number">4.6.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">        } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP4_6_1" class="named-paragraph-link"><span class="named-paragraph">The BP fails type-checking</span><span class="named-paragraph-number">4.6.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP4_6_1" class="paragraph-anchor"></a><b>&#167;4.6.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">The BP fails type-checking</span><span class="named-paragraph-number">4.6.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"BP $o cannot be applied\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4_6">&#167;4.6</a> (three times).</li></ul>
<p class="commentary firstcommentary"><a id="SP4_7" class="paragraph-anchor"></a><b>&#167;4.7. </b>Not so much for the debugging log as for the internal test, in fact, which
prints the log to an I6 string. This is the type-checking report in the case
of success.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Show the variable assignment in the debugging log</span><span class="named-paragraph-number">4.7</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[26], </span><span class="identifier-syntax">c</span><span class="plain-syntax">=0;</span>
<span class="plain-syntax">    </span><a href="4-bas.html#SP1" class="function-link"><span class="function-syntax">Binding::determine_status</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">var_states</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="plain-syntax">&lt;26; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] != </span><span class="constant-syntax">UNUSED_VST</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"%c%s - %u. "</span><span class="plain-syntax">, </span><span class="identifier-syntax">pcalc_vars</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">],</span>
<span class="plain-syntax">                (</span><span class="identifier-syntax">var_states</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] == </span><span class="constant-syntax">FREE_VST</span><span class="plain-syntax">)?</span><span class="string-syntax">" (free)"</span><span class="plain-syntax">:</span><span class="string-syntax">""</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">vta</span><span class="plain-syntax">.</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]); </span><span class="identifier-syntax">c</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">c</span><span class="plain-syntax">&gt;0) </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"\n"</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP4">&#167;4</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. The kind of a term.</b>The following routine works out the kind of value stored in a term, something
which requires contextual information: unless we know the kind of value stored
in each variable, we cannot know the kind of value a general term represents,
which is why the routine is here and not in the Terms section.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">TypecheckPropositions::kind_of_term</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></span>:<br/><a href="4-tcp.html#SP4">&#167;4</a>, <a href="4-tcp.html#SP6">&#167;6</a>, <a href="4-tcp.html#SP9">&#167;9</a>, <a href="4-tcp.html#SP9_2">&#167;9.2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP6" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term_inner</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">term_checked_as_kind</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) { </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">MATCHING</span><span class="plain-syntax">, </span><span class="string-syntax">"No kind for term $0 = $T\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">); </span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">flag_problem</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. </b>The case needing attention is a term in the form \(t = f_B(s)\). By recursion
we can know the kind of \(s\), but we must check that \(f_B\) can validly be applied
to a value of that kind. If \(B\) is a binary predicate with domains \(R\) and \(S\)
(i.e., a subset of \(R\times S\)) then we will either have \(f_B:R\to S\) or vice
versa; so we have to check that \(s\) lies in \(R\) (or \(S\), respectively).
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">TypecheckPropositions::kind_of_term_inner</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::kind_of_term_inner</span></span>:<br/><a href="4-tcp.html#SP5">&#167;5</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">VALUE_TO_KIND_FUNCTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">constant</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">vta</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">assigned_kinds</span><span class="plain-syntax">[</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">variable</span><span class="plain-syntax">];</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kind_found</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP5" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kind_from</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP7" class="function-link"><span class="function-syntax">TypecheckPropositions::approximate_argument_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">from_term</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kind_to</span><span class="plain-syntax"> = </span><a href="4-tcp.html#SP7" class="function-link"><span class="function-syntax">TypecheckPropositions::approximate_argument_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax"> - </span><span class="identifier-syntax">pt</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">from_term</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">kind_from</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">Kinds::compatible</span><span class="plain-syntax">(</span><span class="identifier-syntax">kind_found</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_from</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Term $0 applies function to %u not %u\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">pt</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_found</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_from</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><a href="4-tcp.html#SP10" class="function-link"><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_found</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_to</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kind_found</span><span class="plain-syntax"> = </span><span class="identifier-syntax">kind_from</span><span class="plain-syntax">; </span><span class="comment-syntax"> the better to recover</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">kind_to</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">kind_to</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">kind_found</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. </b>Some relations specify a kind for their terms, others do not. When they do
specify a kind of object, we usually want to be forgiving about nuances of
the kind of object &mdash; for our purposes here, any object will do. (Run-time
type checking takes care of those nuances better.)
</p>

<p class="commentary">The following gives the kind of a given term. It should be used only where
the BP is one constraining its terms, such as when it provides a \(f_B\)
function.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">TypecheckPropositions::approximate_argument_kind</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::approximate_argument_kind</span></span>:<br/><a href="4-tcp.html#SP6">&#167;6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">Kinds::weaken</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">, </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. Type-checking predicates.</b>We take unary predicates first, then binary. Unary predicates are just
adjectives, and all of the work for that has already been done, so we need
only produce a problem message when the worst happens.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::type_check_unary_predicate</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::type_check_unary_predicate</span></span>:<br/><a href="4-tcp.html#SP4_6">&#167;4.6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tr</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-upf.html#SP3" class="function-link"><span class="function-syntax">UnaryPredicateFamilies::typecheck</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tr</span><span class="plain-syntax">, </span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. </b>Binary predicates (BPs) are both easier and harder. Easier because they
have only one definition at a time (unlike, say, the adjective "empty"),
harder because the work hasn't already been done and because some BPs &mdash;
like "is" &mdash; are polymorphic. Here goes:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::type_check_binary_predicate</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::type_check_binary_predicate</span></span>:<br/><a href="4-tcp.html#SP4_6">&#167;4.6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pl</span><span class="plain-syntax">, </span><span class="reserved-syntax">variable_type_assignment</span><span class="plain-syntax"> *</span><span class="identifier-syntax">vta</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_binary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[2], *</span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">[2];</span>

<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP9_2" class="named-paragraph-link"><span class="named-paragraph">Work out what kinds we find</span><span class="named-paragraph-number">9.2</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">VERB_MEANING_UNIVERSAL_CALCULUS_RELATION</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">VERB_MEANING_UNIVERSAL_CALCULUS_RELATION</span><span class="plain-syntax">) </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP9_3" class="named-paragraph-link"><span class="named-paragraph">Adapt to the universal relation</span><span class="named-paragraph-number">9.3</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP9_1" class="named-paragraph-link"><span class="named-paragraph">Work out what kinds we should have found</span><span class="named-paragraph-number">9.1</span></a></span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">result</span><span class="plain-syntax"> = </span><a href="3-bpf.html#SP3" class="function-link"><span class="function-syntax">BinaryPredicateFamilies::typecheck</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">result</span><span class="plain-syntax"> == </span><span class="constant-syntax">NEVER_MATCH_SAYING_WHY_NOT</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">kinds_dereferencing_properties</span><span class="plain-syntax">[2];</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_dereferencing_properties</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">Kinds::dereference_properties</span><span class="plain-syntax">(</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0]);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_dereferencing_properties</span><span class="plain-syntax">[1] = </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1];</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">r2</span><span class="plain-syntax"> = </span><a href="3-bpf.html#SP3" class="function-link"><span class="function-syntax">BinaryPredicateFamilies::typecheck</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_dereferencing_properties</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">r2</span><span class="plain-syntax"> == </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">r2</span><span class="plain-syntax"> == </span><span class="identifier-syntax">SOMETIMES_MATCH</span><span class="plain-syntax">)) </span><span class="identifier-syntax">result</span><span class="plain-syntax"> = </span><span class="identifier-syntax">r2</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">result</span><span class="plain-syntax"> != </span><span class="constant-syntax">DECLINE_TO_MATCH</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">result</span><span class="plain-syntax"> == </span><span class="constant-syntax">NEVER_MATCH_SAYING_WHY_NOT</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">issue_error</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">function</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><a href="4-tcp.html#SP10" class="function-link"><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                    </span><a href="4-tcp.html#SP5" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">),</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">function</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><a href="4-tcp.html#SP10" class="function-link"><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">bp</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0],</span>
<span class="plain-syntax">                    </span><a href="4-tcp.html#SP5" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">function</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">fn_of</span><span class="plain-syntax">), </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">),</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"(%u, %u) failed in $2\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0], </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], </span><span class="identifier-syntax">bp</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">ComparisonFailed_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0], </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">result</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>

<span class="plain-syntax">    </span><span class="named-paragraph-container code-font"><a href="4-tcp.html#SP9_4" class="named-paragraph-link"><span class="named-paragraph">Apply default rule applying to most binary predicates</span><span class="named-paragraph-number">9.4</span></a></span><span class="plain-syntax">;</span>

<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">ALWAYS_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP9_1" class="paragraph-anchor"></a><b>&#167;9.1. </b>Once again we treat any kind of object as just "object", but we do take
note that some BPs &mdash; like "is" &mdash; specify no kinds at all, and so
produce a <span class="extract"><span class="extract-syntax">kinds_required</span></span> which is <span class="extract"><span class="extract-syntax">NULL</span></span>.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Work out what kinds we should have found</span><span class="named-paragraph-number">9.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Kinds::weaken</span><span class="plain-syntax">(</span><a href="3-bp.html#SP7" class="function-link"><span class="function-syntax">BinaryPredicates::term_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">i</span><span class="plain-syntax">), </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">K</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><span class="identifier-syntax">K_object</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] = </span><span class="identifier-syntax">K</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP9">&#167;9</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP9_2" class="paragraph-anchor"></a><b>&#167;9.2. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Work out what kinds we find</span><span class="named-paragraph-number">9.2</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">] =</span>
<span class="plain-syntax">            </span><a href="4-tcp.html#SP5" class="function-link"><span class="function-syntax">TypecheckPropositions::kind_of_term</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]), </span><span class="identifier-syntax">vta</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP9">&#167;9</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP9_3" class="paragraph-anchor"></a><b>&#167;9.3. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Adapt to the universal relation</span><span class="named-paragraph-number">9.3</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::get_construct</span><span class="plain-syntax">(</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0]) != </span><span class="identifier-syntax">CON_relation</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">BadUniversal1_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0], </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::get_construct</span><span class="plain-syntax">(</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1]) != </span><span class="identifier-syntax">CON_combination</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">BadUniversal2_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>

<span class="plain-syntax">    </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">left</span><span class="plain-syntax"> = </span><span class="identifier-syntax">pl</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Node::is</span><span class="plain-syntax">(</span><span class="identifier-syntax">left</span><span class="plain-syntax">, </span><span class="identifier-syntax">CONSTANT_NT</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">VALUE_TO_RELATION_FUNCTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">left</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">cleft</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">cright</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">Kinds::binary_construction_material</span><span class="plain-syntax">(</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], &amp;</span><span class="identifier-syntax">cleft</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">cright</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0] = </span><span class="identifier-syntax">cleft</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1] = </span><span class="identifier-syntax">cright</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP9">&#167;9</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP9_4" class="paragraph-anchor"></a><b>&#167;9.4. </b>The default rule is straightforward: the kinds found have to match the kinds
required.
</p>

<p class="commentary"><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Apply default rule applying to most binary predicates</span><span class="named-paragraph-number">9.4</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">i</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">i</span><span class="plain-syntax">&lt;2; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">])</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Kinds::compatible</span><span class="plain-syntax">(</span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]) == </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">tck</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">log_to_I6_text</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Term %d is %u not %u\n"</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                        </span><span class="identifier-syntax">i</span><span class="plain-syntax">, </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">], </span><span class="identifier-syntax">kinds_required</span><span class="plain-syntax">[</span><span class="identifier-syntax">i</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">                </span><a href="4-tcp.html#SP10" class="function-link"><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">bp</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[0], </span><span class="identifier-syntax">kinds_of_terms</span><span class="plain-syntax">[1], </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEVER_MATCH</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-tcp.html#SP9">&#167;9</a>.</li></ul>
<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. Two problem messages needed more than once.</b></p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::issue_bp_typecheck_error</span></span>:<br/><a href="4-tcp.html#SP6">&#167;6</a>, <a href="4-tcp.html#SP9">&#167;9</a>, <a href="4-tcp.html#SP9_4">&#167;9.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">t0</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">t1</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">BinaryMisapplied2_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">t0</span><span class="plain-syntax">, </span><span class="identifier-syntax">t1</span><span class="plain-syntax">, </span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::issue_kind_typecheck_error</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::issue_kind_typecheck_error</span></span>:<br/><a href="4-tcp.html#SP4_2">&#167;4.2</a></span></button><span class="plain-syntax">(</span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">actually_find</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">need_to_find</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">ka</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax"> = (</span><span class="identifier-syntax">ka</span><span class="plain-syntax">)?(</span><span class="identifier-syntax">ka</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">saved_bp</span><span class="plain-syntax">):</span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bp</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">BinaryMisapplied1_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">actually_find</span><span class="plain-syntax">, </span><span class="identifier-syntax">need_to_find</span><span class="plain-syntax">, </span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">        </span><a href="4-tcp.html#SP11" class="function-link"><span class="function-syntax">TypecheckPropositions::problem</span></a><span class="plain-syntax">(</span><span class="constant-syntax">KindMismatch_CALCERROR</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">EMPTY_WORDING</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">actually_find</span><span class="plain-syntax">, </span><span class="identifier-syntax">need_to_find</span><span class="plain-syntax">, </span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. </b>Some tools using this module will want to push simple error messages out to
the command line; others will want to translate them into elaborate problem
texts in HTML. So the client is allowed to define <span class="extract"><span class="extract-syntax">PROBLEM_SYNTAX_CALLBACK</span></span>
to some routine of her own, gazumping this one.
</p>

<pre class="definitions code-font"><span class="definition-keyword">enum</span> <span class="constant-syntax">BareKindVariable_CALCERROR</span><span class="plain-syntax"> </span><span class="identifier-syntax">from</span><span class="plain-syntax"> </span><span class="constant-syntax">1</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">ConstantFailed_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">UnaryMisapplied_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">ComparisonFailed_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">BadUniversal1_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">BadUniversal2_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">BinaryMisapplied1_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">BinaryMisapplied2_CALCERROR</span>
<span class="definition-keyword">enum</span> <span class="constant-syntax">KindMismatch_CALCERROR</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">TypecheckPropositions::problem</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">TypecheckPropositions::problem</span></span>:<br/><a href="4-tcp.html#SP4_3">&#167;4.3</a>, <a href="4-tcp.html#SP4_1_1">&#167;4.1.1</a>, <a href="4-tcp.html#SP9">&#167;9</a>, <a href="4-tcp.html#SP9_3">&#167;9.3</a>, <a href="4-tcp.html#SP10">&#167;10</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">err_no</span><span class="plain-syntax">, </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">wording</span><span class="plain-syntax"> </span><span class="identifier-syntax">W</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="reserved-syntax">binary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="reserved-syntax">tc_problem_kit</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tck</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">PROBLEM_CALCULUS_CALLBACK</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">PROBLEM_CALCULUS_CALLBACK</span><span class="plain-syntax">(</span><span class="identifier-syntax">err_no</span><span class="plain-syntax">, </span><span class="identifier-syntax">spec</span><span class="plain-syntax">, </span><span class="identifier-syntax">W</span><span class="plain-syntax">, </span><span class="identifier-syntax">K1</span><span class="plain-syntax">, </span><span class="identifier-syntax">K2</span><span class="plain-syntax">, </span><span class="identifier-syntax">bp</span><span class="plain-syntax">, </span><span class="identifier-syntax">tck</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">ifndef</span><span class="plain-syntax"> </span><span class="identifier-syntax">PROBLEM_CALCULUS_CALLBACK</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TEMPORARY_TEXT</span><span class="plain-syntax">(</span><span class="identifier-syntax">text</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">text</span><span class="plain-syntax">, </span><span class="string-syntax">"%+W"</span><span class="plain-syntax">, </span><span class="identifier-syntax">Node::get_text</span><span class="plain-syntax">(</span><span class="identifier-syntax">current_sentence</span><span class="plain-syntax">));</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">err_no</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">BareKindVariable_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"letter variable used where noun expected: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">ConstantFailed_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"constant made no sense: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">UnaryMisapplied_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"unary predicate misapplied: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">ComparisonFailed_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"compared incomparable values: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">BadUniversal1_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"not a relation: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">BadUniversal2_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"not a combination: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">BinaryMisapplied1_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"binary predicate misapplied: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">BinaryMisapplied2_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"binary predicate misapplied: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">KindMismatch_CALCERROR:</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Errors::with_text</span><span class="plain-syntax">(</span><span class="string-syntax">"kind mismatch: %S"</span><span class="plain-syntax">, </span><span class="identifier-syntax">text</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">DISCARD_TEXT</span><span class="plain-syntax">(</span><span class="identifier-syntax">text</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    #</span><span class="identifier-syntax">endif</span>
<span class="plain-syntax">}</span>
</pre>
<nav role="progress"><div class="progresscontainer">
    <ul class="progressbar"><li class="progressprev"><a href="4-bas.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresscurrentchapter">4</li><li class="progresssection"><a href="4-trm.html">trm</a></li><li class="progresssection"><a href="4-ap.html">ap</a></li><li class="progresssection"><a href="4-prp.html">prp</a></li><li class="progresssection"><a href="4-bas.html">bas</a></li><li class="progresscurrent">tcp</li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="5-sc.html">&#10095;</a></li></ul></div>
</nav><!-- End of weave -->

		</main>
	</body>
</html>

